STM: es realizer wf

ABS: 

STM: Rnone wf

ABS: left  right

STM: Rplus wf

ABS: @loc x initially v:T

STM: Rinit wf

ABS: @loc only events in L change x:T

STM: Rframe wf

ABS: only events in L send on lnk with tag

STM: Rsframe wf

ABS: @loc effect knd(v:T)  x := f State(ds) v 

STM: Reffect wf

ABS: sends knd(v:T) on l:tagged(g,State(ds),v):dt

STM: Rsends wf

ABS: @loc precondition for a(v:T):P State(ds) v

STM: Rpre wf

ABS: @loc: k writes only members of L

STM: Raframe wf

ABS: @loc: k sends only on links in L

STM: Rbframe wf

ABS: @loc: only members of L read x

STM: Rrframe wf

ABS: es realizer ind

STM: es realizer ind wf

STM: es realizer-induction

ABS: es realizer ind Rnone compseq tag def

ABS: es realizer ind Rplus compseq tag def

ABS: es realizer ind Rinit compseq tag def

ABS: es realizer ind Rframe compseq tag def

ABS: es realizer ind Rsframe compseq tag def

ABS: es realizer ind Reffect compseq tag def

ABS: es realizer ind Rsends compseq tag def

ABS: es realizer ind Rpre compseq tag def

ABS: es realizer ind Raframe compseq tag def

ABS: es realizer ind Rbframe compseq tag def

ABS: es realizer ind Rrframe compseq tag def

ABS: Rnone?(x1)

STM: Rnone? wf

ABS: Rplus?(x1)

STM: Rplus? wf

ABS: Rplus-left(x1)

STM: Rplus-left wf

ABS: Rplus-right(x1)

STM: Rplus-right wf

ABS: Rinit?(x1)

STM: Rinit? wf

ABS: Rinit-loc(x1)

STM: Rinit-loc wf

ABS: Rinit-T(x1)

STM: Rinit-T wf

ABS: Rinit-x(x1)

STM: Rinit-x wf

ABS: Rinit-v(x1)

STM: Rinit-v wf

ABS: Rframe?(x1)

STM: Rframe? wf

ABS: Rframe-loc(x1)

STM: Rframe-loc wf

ABS: Rframe-T(x1)

STM: Rframe-T wf

ABS: Rframe-x(x1)

STM: Rframe-x wf

ABS: Rframe-L(x1)

STM: Rframe-L wf

ABS: Rsframe?(x1)

STM: Rsframe? wf

ABS: Rsframe-lnk(x1)

STM: Rsframe-lnk wf

ABS: Rsframe-tag(x1)

STM: Rsframe-tag wf

ABS: Rsframe-L(x1)

STM: Rsframe-L wf

ABS: Reffect?(x1)

STM: Reffect? wf

ABS: Reffect-loc(x1)

STM: Reffect-loc wf

ABS: Reffect-ds(x1)

STM: Reffect-ds wf

ABS: Reffect-knd(x1)

STM: Reffect-knd wf

ABS: Reffect-T(x1)

STM: Reffect-T wf

ABS: Reffect-x(x1)

STM: Reffect-x wf

ABS: Reffect-f(x1)

STM: Reffect-f wf

ABS: Rsends?(x1)

STM: Rsends? wf

ABS: Rsends-ds(x1)

STM: Rsends-ds wf

ABS: Rsends-knd(x1)

STM: Rsends-knd wf

ABS: Rsends-T(x1)

STM: Rsends-T wf

ABS: Rsends-l(x1)

STM: Rsends-l wf

ABS: Rsends-dt(x1)

STM: Rsends-dt wf

ABS: Rsends-g(x1)

STM: Rsends-g wf

ABS: Rpre?(x1)

STM: Rpre? wf

ABS: Rpre-loc(x1)

STM: Rpre-loc wf

ABS: Rpre-ds(x1)

STM: Rpre-ds wf

ABS: Rpre-a(x1)

STM: Rpre-a wf

ABS: Rpre-T(x1)

STM: Rpre-T wf

ABS: Rpre-P(x1)

STM: Rpre-P wf

ABS: Raframe?(x1)

STM: Raframe? wf

ABS: Raframe-loc(x1)

STM: Raframe-loc wf

ABS: Raframe-k(x1)

STM: Raframe-k wf

ABS: Raframe-L(x1)

STM: Raframe-L wf

ABS: Rbframe?(x1)

STM: Rbframe? wf

ABS: Rbframe-loc(x1)

STM: Rbframe-loc wf

ABS: Rbframe-k(x1)

STM: Rbframe-k wf

ABS: Rbframe-L(x1)

STM: Rbframe-L wf

ABS: Rrframe?(x1)

STM: Rrframe? wf

ABS: Rrframe-loc(x1)

STM: Rrframe-loc wf

ABS: Rrframe-x(x1)

STM: Rrframe-x wf

ABS: Rrframe-L(x1)

STM: Rrframe-L wf